es:ES, i, j:Id. (i = j)  (state@i r discrete state@j) 

latex

Definitions	ff, , True, T, tt, x. t(x), t  T, Top, if b then t else f fi , discrete state@i, state@i, P  Q, x:A. B(x), P & Q, P  Q, Unit, , x(s),
Lemmas	assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, event system wf, Id wf, true wf, squash wf, eqtt to assert, bool wf, es-vartype wf, subtype rel dep function